Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies

摘要

We present a terminating tableau calculus for graded hybrid logic with globalmodalities, reflexivity, transitivity and role hierarchies. Termination of thesystem is achieved through pattern-based blocking. Previous approaches torelated logics all rely on chain-based blocking. Besides being conceptuallysimple and suitable for efficient implementation, the pattern-based approachgives us a NExpTime complexity bound for the decision procedure.